Termination w.r.t. Q of the following Term Rewriting System could be proven:
Q restricted rewrite system:
The TRS R consists of the following rules:
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Q is empty.
↳ QTRS
↳ DependencyPairsProof
↳ QTRS Reverse
Q restricted rewrite system:
The TRS R consists of the following rules:
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Q is empty.
Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:
PROPER(g(X)) → PROPER(X)
PROPER(f(X)) → F(proper(X))
TOP(mark(X)) → PROPER(X)
TOP(mark(X)) → TOP(proper(X))
F(ok(X)) → F(X)
ACTIVE(c) → F(g(c))
G(ok(X)) → G(X)
PROPER(g(X)) → G(proper(X))
ACTIVE(c) → G(c)
PROPER(f(X)) → PROPER(X)
TOP(ok(X)) → ACTIVE(X)
TOP(ok(X)) → TOP(active(X))
The TRS R consists of the following rules:
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
PROPER(g(X)) → PROPER(X)
PROPER(f(X)) → F(proper(X))
TOP(mark(X)) → PROPER(X)
TOP(mark(X)) → TOP(proper(X))
F(ok(X)) → F(X)
ACTIVE(c) → F(g(c))
G(ok(X)) → G(X)
PROPER(g(X)) → G(proper(X))
ACTIVE(c) → G(c)
PROPER(f(X)) → PROPER(X)
TOP(ok(X)) → ACTIVE(X)
TOP(ok(X)) → TOP(active(X))
The TRS R consists of the following rules:
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 4 SCCs with 6 less nodes.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
G(ok(X)) → G(X)
The TRS R consists of the following rules:
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
G(ok(X)) → G(X)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the usable rules with reduction pair processor [15] with a polynomial ordering [25], all dependency pairs and the corresponding usable rules [17] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.
The following dependency pairs can be deleted:
G(ok(X)) → G(X)
No rules are removed from R.
Used ordering: POLO with Polynomial interpretation [25]:
POL(G(x1)) = 2·x1
POL(ok(x1)) = 2·x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ PisEmptyProof
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QTRS Reverse
Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
G(ok(X)) → G(X)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
F(ok(X)) → F(X)
The TRS R consists of the following rules:
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
F(ok(X)) → F(X)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
F(ok(X)) → F(X)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
PROPER(g(X)) → PROPER(X)
PROPER(f(X)) → PROPER(X)
The TRS R consists of the following rules:
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
TOP(mark(X)) → TOP(proper(X))
TOP(ok(X)) → TOP(active(X))
The TRS R consists of the following rules:
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We have reversed the following QTRS:
The set of rules R is
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The set Q is empty.
We have obtained the following QTRS:
c'(active(x)) → c'(g(f(mark(x))))
g(f(active(x))) → g(mark(x))
c'(proper(x)) → c'(ok(x))
f(proper(x)) → proper(f(x))
g(proper(x)) → proper(g(x))
ok(f(x)) → f(ok(x))
ok(g(x)) → g(ok(x))
mark(top(x)) → proper(top(x))
ok(top(x)) → active(top(x))
The set Q is empty.
↳ QTRS
↳ DependencyPairsProof
↳ QTRS Reverse
↳ QTRS
↳ RFCMatchBoundsTRSProof
Q restricted rewrite system:
The TRS R consists of the following rules:
c'(active(x)) → c'(g(f(mark(x))))
g(f(active(x))) → g(mark(x))
c'(proper(x)) → c'(ok(x))
f(proper(x)) → proper(f(x))
g(proper(x)) → proper(g(x))
ok(f(x)) → f(ok(x))
ok(g(x)) → g(ok(x))
mark(top(x)) → proper(top(x))
ok(top(x)) → active(top(x))
Q is empty.
Termination of the TRS R could be shown with a Match Bound [6,7] of 6. This implies Q-termination of R.
The following rules were used to construct the certificate:
c'(active(x)) → c'(g(f(mark(x))))
g(f(active(x))) → g(mark(x))
c'(proper(x)) → c'(ok(x))
f(proper(x)) → proper(f(x))
g(proper(x)) → proper(g(x))
ok(f(x)) → f(ok(x))
ok(g(x)) → g(ok(x))
mark(top(x)) → proper(top(x))
ok(top(x)) → active(top(x))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
104, 105, 106, 107, 108, 109, 111, 110, 112, 113, 114, 115, 116, 117, 118, 120, 119, 121, 122, 123, 124, 125, 126, 127, 128, 129, 130, 131, 132, 133, 134, 135, 136, 137, 138, 139, 140, 141, 142, 143, 144, 145, 146, 147, 148, 149, 150, 151, 152, 154, 156, 160, 163
Node 104 is start node and node 105 is final node.
Those nodes are connect through the following edges:
- 104 to 106 labelled proper_1(0)
- 104 to 107 labelled active_1(0), proper_1(0)
- 104 to 108 labelled g_1(0), f_1(0), c'_1(0)
- 104 to 109 labelled c'_1(0)
- 104 to 117 labelled c'_1(1)
- 104 to 116 labelled proper_1(1)
- 104 to 118 labelled c'_1(1)
- 104 to 120 labelled g_1(1)
- 104 to 126 labelled proper_1(2)
- 104 to 127 labelled c'_1(2)
- 104 to 139 labelled c'_1(3)
- 104 to 156 labelled c'_1(4)
- 105 to 105 labelled #_1(0)
- 106 to 105 labelled g_1(0), f_1(0)
- 106 to 113 labelled proper_1(1)
- 106 to 114 labelled g_1(1)
- 106 to 122 labelled proper_1(2)
- 107 to 105 labelled top_1(0)
- 108 to 105 labelled ok_1(0), mark_1(0)
- 108 to 112 labelled proper_1(1), active_1(1)
- 108 to 115 labelled g_1(1), f_1(1)
- 108 to 124 labelled g_1(2)
- 108 to 131 labelled proper_1(3)
- 108 to 135 labelled proper_1(2)
- 109 to 110 labelled g_1(0)
- 109 to 123 labelled proper_1(1)
- 111 to 105 labelled mark_1(0)
- 111 to 112 labelled proper_1(1)
- 110 to 111 labelled f_1(0)
- 110 to 116 labelled proper_1(1)
- 112 to 105 labelled top_1(1)
- 113 to 105 labelled g_1(1), f_1(1)
- 113 to 113 labelled proper_1(1)
- 113 to 114 labelled g_1(1)
- 113 to 122 labelled proper_1(2)
- 114 to 105 labelled mark_1(1)
- 114 to 112 labelled proper_1(1)
- 115 to 105 labelled ok_1(1)
- 115 to 112 labelled active_1(1)
- 115 to 115 labelled g_1(1), f_1(1)
- 115 to 124 labelled g_1(2)
- 115 to 131 labelled proper_1(3)
- 115 to 135 labelled proper_1(2)
- 116 to 112 labelled f_1(1), g_1(1)
- 116 to 131 labelled f_1(1), g_1(1)
- 116 to 135 labelled g_1(1), f_1(1)
- 117 to 112 labelled ok_1(1)
- 117 to 121 labelled active_1(2)
- 117 to 123 labelled ok_1(1)
- 117 to 133 labelled g_1(2)
- 117 to 131 labelled ok_1(1)
- 117 to 135 labelled ok_1(1)
- 117 to 141 labelled f_1(2), g_1(2)
- 117 to 136 labelled f_1(2), g_1(2)
- 117 to 142 labelled g_1(3)
- 117 to 145 labelled proper_1(4)
- 118 to 119 labelled g_1(1)
- 118 to 130 labelled proper_1(2)
- 120 to 112 labelled mark_1(1)
- 120 to 121 labelled proper_1(2)
- 119 to 120 labelled f_1(1)
- 119 to 125 labelled proper_1(2)
- 121 to 105 labelled top_1(2)
- 122 to 112 labelled g_1(2)
- 123 to 116 labelled g_1(1)
- 124 to 112 labelled mark_1(2)
- 124 to 121 labelled proper_1(2)
- 125 to 121 labelled f_1(2)
- 126 to 121 labelled g_1(2)
- 127 to 128 labelled g_1(2)
- 127 to 130 labelled ok_1(2)
- 127 to 137 labelled proper_1(3)
- 127 to 138 labelled g_1(3)
- 127 to 148 labelled g_1(4)
- 127 to 145 labelled ok_1(2)
- 127 to 150 labelled proper_1(5)
- 128 to 129 labelled f_1(2)
- 128 to 134 labelled proper_1(3)
- 129 to 121 labelled mark_1(2)
- 129 to 132 labelled proper_1(3)
- 130 to 125 labelled g_1(2)
- 131 to 121 labelled g_1(3)
- 132 to 105 labelled top_1(3)
- 133 to 116 labelled ok_1(2)
- 133 to 136 labelled f_1(2), g_1(2)
- 133 to 121 labelled ok_1(2)
- 133 to 132 labelled active_1(3)
- 133 to 141 labelled f_1(2), g_1(2)
- 134 to 132 labelled f_1(3)
- 135 to 131 labelled f_1(2), g_1(2)
- 135 to 135 labelled g_1(2), f_1(2)
- 136 to 112 labelled ok_1(2)
- 136 to 121 labelled active_1(2)
- 136 to 131 labelled ok_1(2)
- 136 to 140 labelled g_1(3)
- 137 to 134 labelled g_1(3)
- 138 to 125 labelled ok_1(3)
- 138 to 140 labelled f_1(3)
- 138 to 132 labelled ok_1(3)
- 138 to 149 labelled active_1(4)
- 139 to 137 labelled ok_1(3)
- 139 to 144 labelled g_1(4)
- 139 to 151 labelled g_1(5)
- 139 to 150 labelled ok_1(3)
- 139 to 154 labelled proper_1(6)
- 140 to 121 labelled ok_1(3)
- 140 to 132 labelled active_1(3)
- 141 to 135 labelled ok_1(2)
- 141 to 143 labelled f_1(3), g_1(3)
- 142 to 121 labelled mark_1(3)
- 142 to 132 labelled proper_1(3)
- 143 to 135 labelled ok_1(3)
- 143 to 131 labelled ok_1(3)
- 143 to 143 labelled f_1(3), g_1(3)
- 143 to 147 labelled g_1(4)
- 144 to 134 labelled ok_1(4)
- 144 to 146 labelled f_1(4)
- 144 to 149 labelled ok_1(4)
- 144 to 152 labelled active_1(5)
- 145 to 132 labelled g_1(4)
- 146 to 132 labelled ok_1(4)
- 146 to 149 labelled active_1(4)
- 147 to 121 labelled ok_1(4)
- 147 to 132 labelled active_1(3)
- 148 to 132 labelled mark_1(4)
- 148 to 149 labelled proper_1(4)
- 149 to 105 labelled top_1(4)
- 150 to 149 labelled g_1(5)
- 151 to 149 labelled mark_1(5)
- 151 to 152 labelled proper_1(5)
- 152 to 105 labelled top_1(5)
- 154 to 152 labelled g_1(6)
- 156 to 154 labelled ok_1(4)
- 156 to 160 labelled g_1(5)
- 160 to 152 labelled ok_1(5)
- 160 to 163 labelled active_1(6)
- 163 to 105 labelled top_1(6)